/* -*- Mode: C++; c-basic-offset: 2 -*- */

#include "Common.h"
#include "klee/Internal/Module/KInstruction.h"
#include "tern/RaceDetector.h"
#include "tern/TernUtil.h"

#include "llvm/Support/raw_ostream.h"
#include "llvm/Instruction.h"
#include "llvm/BasicBlock.h"
#include "llvm/Function.h"

#include <iostream>
#include <sstream>

//#define dprintf(args...) fprintf(stderr, args)
#define dprintf(args...)

using namespace llvm;
using namespace klee;

void VectorClock::tick(int idx)
{ 
  assert(0 <= idx && idx < width && "VectorClock::tick(idx) is off bound!"); 
  ++ clocks[idx]; 
}

void VectorClock::setWidth(int n)
{ 
  assert(n <= MAX_THREADS && "VectorClock::setWidth(n) is too wide!");
  for(;width < n; ++width)
    clocks[width] = 0;
  width = n;
}

void VectorClock::merge(const VectorClock& vc)
{
  for(int i=0; i<width && i<vc.width; ++i) {
    if(clocks[i] < vc.clocks[i])
      clocks[i] = vc.clocks[i];
  }
  for(; width<vc.width; ++width) 
    clocks[width] = vc.clocks[width];
}

bool VectorClock::happensbefore(const VectorClock& vc) const
{
  // each clock is smaller than or equal to the corresponding one in vc
  for(int i=0; i<width && i<vc.width; ++i) {
    if(clocks[i] > vc.clocks[i])
      return false;
  }
  // and the length of this vector clock is the same or smaller than vc
  return width<=vc.width;
}

bool VectorClock::concurrent(const VectorClock& vc) const
{
  return ! (happensbefore(vc) || vc.happensbefore(*this));
}

void VectorClock::print(std::ostream &o)
{
  o<<"[";
  std::copy(clocks, clocks+width, std::ostream_iterator<int>(o, ","));
  o<<"]";
}

std::string VectorClock::toString()
{
  std::stringstream s;
  print(s);
  return s.str();
}

/***/

Access::Access(int t, bool i, const VectorClock& s, KInstruction *inst,
               ref<Expr> v, ref<Expr> old_v) 
  : tid(t), isWrite(i), ts(s), ki(inst), value(v), old_value(old_v)
{
}

Access::Access(const Access &a)
  : tid(a.tid), isWrite(a.isWrite), ts(a.ts), ki(a.ki), 
    value(a.value), old_value(a.old_value)
{
}

/***/

AccessHistory::AccessHistory(const MemoryObject *m, ref<Expr> o, int w)
  : mo(m), offset(o), width(w), write(NULL) 
{
}

AccessHistory::AccessHistory(const MemoryObject *m, ref<Expr> o, 
                             int w, Access *a)
{
  mo = m;
  offset = o;
  width = w;
  if(a->isWrite) {
    write = a;
  } else {
    write = NULL;
    reads.push_back(a);
  }
}

AccessHistory::AccessHistory(const MemoryObject *m, long o, int w)
{
  mo = m;
  offset = ConstantExpr::create(o, Expr::Int64);
  width = w;
  write = NULL;
}

AccessHistory::AccessHistory(const MemoryObject *m, long o, 
                             int w, Access *a)
{
  mo = m;
  offset = ConstantExpr::create(o, Expr::Int64);
  width = w;
  if(a->isWrite) {
    write = a;
  } else {
    write = NULL;
    reads.push_back(a);
  }
}

AccessHistory::AccessHistory(const AccessHistory &ah)
{
  mo = ah.mo;
  offset = ah.offset;
  width = ah.width;
  
  if(ah.write != NULL) {
    write = new Access(*ah.write);
  } else {
    write = NULL;
  }

  std::list<Access*>::const_iterator i;
  for(i=ah.reads.begin(); i!=ah.reads.end(); ++i) {
    Access *read = new Access(**i);
    reads.push_back(read);
  }
}

AccessHistory::~AccessHistory()
{
  if(write)
    delete write;
  
  forall(std::list<Access*>, i, reads)
    delete *i;
}

void AccessHistory::removeReads(Access *access)
{
  std::list<Access*>::iterator cur, prv;
  for(cur=reads.begin(); cur!=reads.end();) {
    prv = cur++;
    if((*prv)->ts.happensbefore(access->ts)) {
      Access *read = *prv;
      delete read;
      reads.erase(prv);
    }
  }
}

void AccessHistory::printRace(Access *a1, Access *a2)
{
  long off = (long)cast<ConstantExpr>(offset)->getZExtValue();
  uint64_t v1_old = cast<ConstantExpr>(a1->old_value)->getZExtValue(width*8);
  uint64_t v1 = cast<ConstantExpr>(a1->value)->getZExtValue(width*8);
  uint64_t v2 = cast<ConstantExpr>(a2->value)->getZExtValue(width*8);

  klee_warning("RACE: conflicting %s (%s) val=0x%lx by thread %d " \
               "and %s (%s) val=0x%lx by thread %d to obj 0x%lx [%lx, %lx)!",
               a1->isWrite?"write":"read",
               a1->ts.toString().c_str(),
               (long)v1,
               a1->tid,
               a2->isWrite?"write":"read",
               a2->ts.toString().c_str(),
               a2->isWrite?(long)v2:(long)v1_old,
               a2->tid,
               mo->address, off, off+width);

  Instruction *i1 = a1->ki->inst, *i2 = a2->ki->inst;
  errs() << "Instuction 1: " << *i1 << "\n"
         << "        in BB " << i1->getParent()->getName() << "\n"
         << "        in FN " << i1->getParent()->getParent()->getName() << "\n";
  errs() << "Instuction 2: " << *i2 << "\n"
         << "        in BB " << i2->getParent()->getName() << "\n"
         << "        in FN " << i2->getParent()->getParent()->getName() << "\n";
}

bool AccessHistory::appendAccess(Access *access)
{
  bool has_race = false;
  Access *racy_access = NULL;

  if(access->isWrite) {
    // remove reads < access->ts
    removeReads(access);

    if(access->isWrite && !reads.empty()) {
      racy_access = reads.front();
      reads.pop_front();
      // suppress later race repors
      std::list<Access*>::iterator i;
      while((i=reads.begin()) != reads.end()) {
        Access *read = *i;
        reads.erase(i);
        delete read;
      }
    }

    // remove write < access->ts
    if(!write || write->ts.happensbefore(access->ts)) {
      delete write;
      write = access;
    } else if (write) {
      racy_access = write;
      // surpress later race reports
       write = access;
    }
  } else {// access->isWrite == false
    removeReads(access);
    if(write && write->ts.concurrent(access->ts)) {
      racy_access = write;
      // suppress later race reports
      write = NULL;
    }
  }

  if(racy_access) {

    has_race = true;
    assert(racy_access->tid != access->tid);

    /// prune benign races.  note that our goal here is decide if the
    /// program may be nondeterministic when two instructions interleave
    /// differently.  we can prune away useless writes: (1) a write-write
    /// race where two writes are of the same value and (2) a read-write
    /// race where the write is of the same value as the value already
    /// read

    // \todo: should consider symbolic values when pruning

    if(get_option(tern, prune_useless_writes)) {
      uint64_t v1, v2;
      if(access->isWrite) { // write-write race or read-write race
        v1 = cast<ConstantExpr>(racy_access->value)->getZExtValue(width*8);
        v2 = cast<ConstantExpr>(access->value)->getZExtValue(width*8);
      } else {  // write-read race
        v1 = cast<ConstantExpr>(racy_access->old_value)->getZExtValue(width*8);
        v2 = cast<ConstantExpr>(racy_access->value)->getZExtValue(width*8);
      }

      if(v1==v2) {
        klee_warning("pruned %s-%s race with value %ld\n", 
                     racy_access->isWrite?"write":"read",
                     access->isWrite?"write":"read",
                     (long)v1);
        has_race = false;
      }
    }

    if(has_race)
      printRace(racy_access, access);
    delete racy_access;
  }

  return has_race;
}

/***/

// FIXME: does it have to be this complicated?
bool ObjectAccessHistory::overlapRangeAccess(const MemoryObject *o, 
                                             long off, int w, Access *access)
{
  bool has_race = false;

  typedef std::pair<long, AccessHistory*> OffsetAccessHistoryPair;
  std::list<OffsetAccessHistoryPair> todo;

  // lower_bound returns the smallest object base address that > off
  ConcreteAccessMap::iterator b = concreteAccesses.lower_bound(off);
  ConcreteAccessMap::iterator e = concreteAccesses.upper_bound(off+w);

  if(b != concreteAccesses.begin())
    --b;
  if(e != concreteAccesses.end())
    ++e;
  assert(b!=e && "no range overlaps with the new range!");
  for(; b!=e; ++b) {
    long old_off = b->first;
    AccessHistory *old_ah = b->second;
    long old_w = old_ah->width;

    if(old_off+old_w <= off)
      continue; // left of off
    if(old_off >= off+w)
      continue; // right of off+w
    // add overlapped ranges
    todo.push_back(*b);
  }

  // remove first and add these ranges back later
  forall(std::list<OffsetAccessHistoryPair>, i, todo)
    concreteAccesses.remove(i->first);

  // iterate through all overlapping ranges and perform add/merge as necessary
  forall(std::list<OffsetAccessHistoryPair>, i, todo) {
    long old_off = i->first;
    AccessHistory *old_ah = i->second;
    long old_w = old_ah->width;

    // intersect [old_off, old_off+old_w) and [off, off+w);
    dprintf("RaceDetector: ranges [%lx, %lx)  and [%lx, %lx)\n",
            old_off, old_off+old_w, off, off+w);

    // start from non-overlap range on the left
    if(old_off < off) {
      // add range [old_off, off) with old hisotry
      dprintf("RaceDetector: split [%lx, %lx) off [%lx, %lx)\n",
              old_off, off, old_off, old_off+old_w);
      AccessHistory *ah = new AccessHistory(*old_ah);
      ah->width = off-old_off;
      concreteAccesses 
        = concreteAccesses.insert(OffsetAccessHistoryPair(old_off, ah));
      // update ranges
      old_w -= off-old_off;
      old_off = off;
    } else if(off < old_off) {
      // add range [off, old_off) with new access
      dprintf("RaceDetector: add [%lx, %lx)\n", off, old_off);
      Access *access_copy = new Access(*access);
      AccessHistory *ah = new AccessHistory(o, off, old_off-off, access_copy);
      concreteAccesses 
        = concreteAccesses.insert(OffsetAccessHistoryPair(off, ah));
      // update ranges
      w -= old_off - off;
      off = old_off;
    }

    // now old_off == off
    if(w <= old_w) { // existing range is longer than us, done
      if(w < old_w) {
        // add range [off+w, off+old_w) with old hisotry
        dprintf("RaceDetector: split [%lx, %lx) off [%lx, %lx)\n",
                off+w, off+old_w, off, off+old_w);
        AccessHistory *ah = new AccessHistory(*old_ah);
        ah->offset = ConstantExpr::create(off+w, Expr::Int64);
        ah->width = old_w - w;
        concreteAccesses 
          = concreteAccesses.insert(OffsetAccessHistoryPair(off+w, ah));
      }
      
      // merge range [off, w) with access
      dprintf("RaceDetector: merge [%lx, %lx)\n", off, off+w);
      old_ah->offset = ConstantExpr::create(off, Expr::Int64);
      old_ah->width = w;
      has_race |= old_ah->appendAccess(access);
      concreteAccesses 
        = concreteAccesses.insert(OffsetAccessHistoryPair(off, old_ah));
      return has_race;
    } else { // old_w < w, existing range is shorter, has to keep looping
      // merge range [off, off+old_w) with access
      dprintf("RaceDetector: merge [%lx, %lx)\n", off, off+old_w);
      old_ah->offset = ConstantExpr::create(off, Expr::Int64);
      old_ah->width = old_w;
      Access *access_copy = new Access(*access);
      has_race |= old_ah->appendAccess(access_copy);
      concreteAccesses 
        = concreteAccesses.insert(OffsetAccessHistoryPair(off, old_ah));
      
      // update remain ranges
      off += old_w;
      w -= old_w;
      dprintf("RaceDetector: remaining [%lx, %lx)\n", off, off+w);
    }
  }

  return has_race;
}

bool ObjectAccessHistory::appendAccess(const MemoryObject *o, ref<Expr> offset, 
                                       int w, Access *access)
{

  if(!isa<ConstantExpr>(offset)) {
    // symbolic memory access.  FIXME: currently not handled yet.
    klee_error("symbolic memory accesses are currently not handled!");
    return false;
  }

  // concrete memory access
  long off = (long)cast<ConstantExpr>(offset)->getZExtValue();
  dprintf("RaceDetector: thread %d %s obj 0x%lx [%lx, %lx) at time %s\n", 
          access->tid, (access->isWrite?"writes":"reads"), 
          o->address, off, off+w, access->ts.toString().c_str());

  // fastpath: access an old range
  const ConcreteAccessMap::value_type *prv 
    = concreteAccesses.lookup_previous(off);
  if(prv) {
    long old_off = prv->first;
    AccessHistory *old_ah = prv->second;
    if(old_off == off && old_ah->width == w) {
      // access an old range
      dprintf("RaceDetector: access old range \n");
      AccessHistory *ah = prv->second;
      return ah->appendAccess(access);
    }
  }

  // fastpath: access an new rage
  const ConcreteAccessMap::value_type *nxt 
    = concreteAccesses.lookup_previous(off+w-1);
  if(prv == nxt) {
    bool is_new = (prv == NULL);
    if(!is_new) {
      long old_off = prv->first;
      AccessHistory *old_ah = prv->second;
      is_new = (old_off+old_ah->width <= off);
    }
    if(is_new) {
      // access a new range
      dprintf("RaceDetector: access new range \n");
      AccessHistory *ah = new AccessHistory(o, offset, w, access);
      concreteAccesses 
        = concreteAccesses.insert(std::pair<long, AccessHistory*>(off, ah));
      return false;
    }
  }

  // slowpath: overlapping but not identical access
  return overlapRangeAccess(o, off, w, access);
}

ObjectAccessHistory::~ObjectAccessHistory() {
  forall(ConcreteAccessMap, i, concreteAccesses) {
    delete i->second;
  }
  forall(SymbolicAccessList, i, symbolicAccesses) {
    delete *i;
  }
}

/***/

void RaceDetector::onMemoryAccess(ExecutionState &state, int tid, bool isWrite, 
               const MemoryObject *mo, ref<Expr> offset, int width, 
               ref<Expr> value, ref<Expr> old_value)
{
  ObjectAccessHistory *oah;
  const ObjectAccessMap::value_type *v = objectAccesses.lookup(mo);
  if(!v) {
    oah = new ObjectAccessHistory;
    objectAccesses 
      = objectAccesses.insert(ObjectAccessMap::value_type(mo, oah));
  } else {
    oah = v->second;
  }
    
  Access *access = new Access(tid, isWrite, threadClocks[tid], state.prevPC,
                              value, old_value);
  racy = oah->appendAccess(mo, offset, width, access);
}

void RaceDetector::onCreateThread(int parent_tid, int child_tid)
{
  assert(parent_tid>=0 && parent_tid<MAX_THREADS);
  assert(child_tid>=0 && parent_tid<MAX_THREADS);
  VectorClock &parent_vc = threadClocks[parent_tid];
  VectorClock &child_vc = threadClocks[child_tid];
  // parent_vc.tick(parent_tid); // parent thread has to get turn before
                                 // creating the child, thus no need to tick
  child_vc.merge(parent_vc);
  dprintf("RaceDetector: thread %d creates thread %d at clock %s\n",
          parent_tid, child_tid, 
          threadClocks[child_tid].toString().c_str());
}

void RaceDetector::onAcquireTurn(int tid)
{

  threadClocks[tid].tick(tid);
  threadClocks[tid].merge(turnClock);
  dprintf("RaceDetector: thread %d gets turn at clock %s\n",
          tid, threadClocks[tid].toString().c_str());
}

void RaceDetector::onReleaseTurn(int tid)
{
  turnClock = threadClocks[tid];
  threadClocks[tid].tick(tid);
  dprintf("RaceDetector: thread %d gives up turn at clock %s\n",
          tid, threadClocks[tid].toString().c_str());
}

RaceDetector::RaceDetector() 
{
  racy = false;
  // initializes vector clocks for all threads
  for(int i=0; i<MAX_THREADS; ++i) {
    threadClocks[i].setWidth(i+1);
    threadClocks[i].tick(i);
  }
}

RaceDetector::~RaceDetector()
{
  forall(ObjectAccessMap, i, objectAccesses) {
    delete i->second;
  }
}

RaceDetector *klee::theRaceDetector = NULL;
